Nuprl Lemma : sum_difference
4,23
postcript
pdf
n
:
,
f
,
g
:(
n
),
d
:
. sum(
f
(
x
)-
g
(
x
) |
x
<
n
) =
d
sum(
f
(
x
) |
x
<
n
) = sum(
g
(
x
) |
x
<
n
)+
d
latex
Definitions
x
.
t
(
x
)
,
x
(
s
)
,
{
i
..
j
}
,
,
A
B
,
A
,
False
,
sum(
f
(
x
) |
x
<
k
)
,
Prop
,
t
T
,
SQType(
T
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
{
T
}
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
sum
functionality
,
sum
linear
,
nat
wf
,
int
seg
wf
,
sum
wf
origin
n:
, f, g:(n
), d:. sum(f(x)-g(x) | x < n) = d 
sum(f(x) | x < n) = sum(g(x) | x < n)+d n:, f, g:(n), d:. sum(f(x)-g(x) | x < n) = d sum(f(x) | x < n) = sum(g(x) | x < n)+d 
x. t(x)
}
B
A
Tx:A. B(x) Q
Q Q